On the strength of “sometimes” and “always” in program verification

Does the application of time quantifiers, such as “sometimes” and “always” in loop invariants, increase the strength of the classical Naur-Floyd-Hoare induction assertion method for proving partial correctness of programs? This question is answered in the affirmative within the precise framework of nonstandard Dynamic Logic. It is also proved that the strengths of invariants with “sometimes” and with “always” are not comparable